package com.googlecode.kipler.satisfiability.completion.branching;

import java.util.ArrayList;
import java.util.List;

import com.googlecode.kipler.container.dl.BasicWcsInterpolationData;
import com.googlecode.kipler.container.dl.DependencySet;
import com.googlecode.kipler.container.dl.LabelManager;
import com.googlecode.kipler.container.dl.MarkedFormulaContainer;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.satisfiability.interpolation.rule.FlatTracingInterpolantCalculation;
import com.googlecode.kipler.satisfiability.interpolation.rule.UnionInterpolantRule;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.Formula;
import com.googlecode.kipler.transformations.FormulaSimplificationVisitor;

public class BetaBranchingPoint extends BranchingPoint {

	private int index;

	private DependencySet dependencySet = new DependencySet();

	private Formula branchCause;

	private List<Formula> formulas = new ArrayList<Formula>();

	private boolean marking;

	private UnionInterpolantRule unionIntRule = new UnionInterpolantRule();

	private WorldConstraintSystem activeWcs;

	private boolean interpolation;

	public BetaBranchingPoint(boolean marking) {
		setMarking(marking);
	}

	public Formula getBranchCause() {
		return branchCause;
	}

	public void setBranchCause(Formula branchCause) {
		this.branchCause = branchCause;
	}

	public boolean addFormula(Formula o) {
		return formulas.add(o);
	}

	protected List<Formula> getFormulas() {
		return formulas;
	}

	private DependencySet getDependencySet() {
		return dependencySet;
	}

	public boolean isMarking() {
		return marking;
	}

	public void setMarking(boolean markBranchCause) {
		this.marking = markBranchCause;
	}

	@Override
	public boolean isBranchingPossible() {
		return index < getFormulas().size();
	}

	public WorldConstraintSystem nextBranch() throws UnsatisfiableException {
		WorldConstraintSystem result = null;
		if (index < 2) {
			Formula f = getFormulas().get(index);
			if (index == 0) {
				result = getWcs().copy();
				result.setId(getWcs().getId() + 1);
				result.getData().getDependencyManager().add(f, getWcs());
				activeWcs = result;
				interpolation = activeWcs.getReasoner().getProfile()
						.isInterpolationEnabled();
				if (interpolation) {
					LabelManager labelMan = ((BasicWcsInterpolationData) result
							.getData()).getLabelManager();
					labelMan.copyLabel(getBranchCause(), f);
				}
			} else if (index == 1) {
				getDependencySet().addAll(getLastBranchDependencies());
				getDependencySet().remove(getWcs());
				result = getWcs();
				Formula negFirstFormula = makeNegFormula();
				result.getData().getDependencyManager().addAll(negFirstFormula,
						getDependencySet());
				result.getData().getDependencyManager().addAll(f,
						getDependencySet());
				result.getData().getDependencyManager().move(f,
						getBranchCause());
				if (interpolation) {
					FlatTracingInterpolantCalculation iCalculator = new FlatTracingInterpolantCalculation();
					iCalculator
							.setPreviousInterpolant(((BasicWcsInterpolationData) getWcs()
									.getData()).getInterpolant());
					iCalculator.setWcs(activeWcs);
					ConceptAssertion interpolant = iCalculator.apply();
					unionIntRule.addCondition(getBranchCause());
					unionIntRule.addPreviousInterpolant(interpolant);

					LabelManager labelMan = ((BasicWcsInterpolationData) result
							.getData()).getLabelManager();
					labelMan.copyLabel(getBranchCause(), f);
					labelMan.copyLabel(getBranchCause(), negFirstFormula);
				}
				activeWcs = result;
				result.getWorld(getWorld().getName()).add(negFirstFormula);
			}
			if (isMarking()) {
				MarkedFormulaContainer wcsData = (MarkedFormulaContainer) result
						.getData();
				wcsData.getMarkedFormulas().add(getBranchCause());
			}
			index++;
			result.getWorld(getWorld().getName()).add(f);
		}
		return result;
	}

	private Formula makeNegFormula() {
		Formula negFirstFormula = getFormulas().get(0).copy().toggleNegated();
		FormulaSimplificationVisitor visitor = new FormulaSimplificationVisitor();
		negFirstFormula.accept(visitor);
		negFirstFormula = visitor.getNormalForm();
		return negFirstFormula;
	}

	public void backtrack() {
		if (interpolation) {
			FlatTracingInterpolantCalculation iCalculator = new FlatTracingInterpolantCalculation();
			iCalculator
					.setPreviousInterpolant(((BasicWcsInterpolationData) getWcs()
							.getData()).getInterpolant());
			iCalculator.setWcs(activeWcs);
			ConceptAssertion interpolant = iCalculator.apply();
			unionIntRule.setWcs(activeWcs);
			unionIntRule.addPreviousInterpolant(interpolant);
			interpolant = unionIntRule.apply();
			if (hasPreviousBranchingPoint()) {
				((BasicWcsInterpolationData) previousBranchingPoint().getWcs()
						.getData()).setInterpolant(interpolant);
			}
		}
	}
}
